\begin{tabbing} p{-}inject($A$;$B$;$f$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$x$:$A$, $y$:$A$.\+ \\[0ex]($\uparrow$can{-}apply($f$;$x$)) \\[0ex]$\Rightarrow$ ($\uparrow$can{-}apply($f$;$y$)) \\[0ex]$\Rightarrow$ (do{-}apply($f$;$x$) = do{-}apply($f$;$y$) $\in$ $B$) \\[0ex]$\Rightarrow$ ($x$ = $y$ $\in$ $A$) \- \end{tabbing}